COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	verifi[e82,jmc]		proofs checkable in linear time
C00010 ENDMK
C⊗;
verifi[e82,jmc]		proofs checkable in linear time

	Suppose someone tells us he has all solutions to (say)
the 27 queens problem, and we ask him to prove it.  One way is
for him to prove that his program is correct, and we run the
program.  The time and storage required for verification of this
(possibly) short proof are (presumably) dominated by those of the
computation of the solution.  However, there may be proofs that
are shorter in terms of time and storage required for verification.
Indeed much of the branching involved in the verification can be
avoided by recording which way the branches go.

	Therefore, we are interested in what we might call an
absolute proof system.  Its verification time is linear in the
size of a proof, and there is no branching except when an actual
error is found.  The idea is that the time of verification cannot
be further shortened by providing additional information.  There
must be such optimal proofs (for a given language), because the
time cannot be reduced to zero.  We would also like the verification
process to be read-only, but it isn't now clear that this is
compatible with the desire to avoid arrays.

	Another way of looking at it is that we want the original
prover to do as much as possible of the work, so that the work
done by the program that checks the proof is as little as possible.
One motivation for this is that comparing the shortest such proof
with the best known algorithm provides a measure of the maximum
possible improvement of the algorithm.  All this relates to
non-deterministic algorithms, because they can be regarded as
proof verifiers.  There is reason to hope that the theory of
the length of minimal verification will be easier than the theory
of most efficient algorithms, because the latter still has no
way of precluding good guessing.  Indeed this is the  P = NP
problem.

	There is an example and a lemma.

Example: Suppose we wish to verify that one list or array is a
sorted version of another.  Here is information that permits the
verification in linear time and space given our computational
model.  It seems that we need either to be able to mark members
of a list as visited or to be able to use arrays and check
array bounds.

	We have two lists (respectively arrays).  One has as elements
those of the original list in sorted order and the other gives them in
original order.  Paired with each element in each list is a pointer to the
corresponding element in the other list.  We first verify that the
allegedly sorted list (array) is in increasing order by running down it.
Next we mwst verify the 1-1 correspondence.

	In the list version each word of (say) the unsorted list has a one
bit marker field and we next make sure that all marks are zero.
Then we run down (say) the sorted list
checking that each word  x  points to a word  y  with the same value part and
is followed by a pointer back to  x.  We also mark each word  y  to show
that it has been visited.  Finally, we run down the second list and check
that each word has been marked.

	In the array version each list occupies the storage between
stated bounds, and we need only check that each pointer points into
the region reserved for the other list.


Lemma: Any verification system that uses arrays can
be replaced by one that uses only pointers and one bit markers.

Proof: The key operation with arrays that can't be done efficiently with
list structures is the computation of an index  i  and its
subsequent use.  Imitating this with list structure in computation
may involve running down the list till the  i th  element is
reached.  A more complicated scheme uses trees but still takes  log n
time to reach an element.

	In a verification system, however, the pointer corresponding
to  i  can be supplied, and the cell pointed to can also have a pointer
back.  In the scan of the list, and we suppose that all lists get
scanned - we can compute the index as we go along, and then compare
its value with that of the index  i  which is found, because there
is a remark in the  i th  cell of the list that in a certain cell there
is a pointer back to this cell and an integer that claims to be the
position of this cell in the list.  We still need one bit markers in
order to be sure that the pointers go to the list in question.
Of course, this assumes that adding to
integers of size up to the size of the proof structure is an elementary
operation and that the cells can store integers of this size.
These assumptions seem appropriate in a context that regards 
following a pointer as an elementary operation.